<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=gb2312" />
<title>Demo -- Geometry Description Language</title>
<script type="text/javascript">
function Prove(){
			var xmlhttp;
			if (window.XMLHttpRequest){// code for IE7+, Firefox, Chrome, Opera, Safari
			  	xmlhttp=new XMLHttpRequest();
			 }else{// code for IE6, IE5
			  	xmlhttp=new ActiveXObject("Microsoft.XMLHTTP");
			 }
			 xmlhttp.onreadystatechange=function(){
			  if (xmlhttp.readyState==4 && xmlhttp.status==200)
				{
				    
					document.getElementById("proofDiv").innerHTML=xmlhttp.responseText;
				}
			  }
			xmlhttp.open("GET","/GDL/prove.jsp?statement="+document.getElementById('statement').value+"&system="+document.getElementById('GATP').value,true);
			xmlhttp.send();
		}
function Open(ref){
			var xmlhttp;
			if (window.XMLHttpRequest){// code for IE7+, Firefox, Chrome, Opera, Safari
			  	xmlhttp=new XMLHttpRequest();
			 }else{// code for IE6, IE5
			  	xmlhttp=new ActiveXObject("Microsoft.XMLHTTP");
			 }
			 var script = document.getElementById('script').value;
			 if(script=="drawing"){
				xmlhttp.open("GET","script4draw.txt",false);
			}else
			if(script=="proving"){
				xmlhttp.open("GET","script4prove.txt",false);
			}
			xmlhttp.send();
			document.getElementById("scriptDiv").innerHTML=xmlhttp.responseText;
		}
function input(name){
		if(name=='Centroid'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Centroid,Prove,configuration(A:=point(),B:=point(),C:=point()),concurrent(medians(triangle(A,B,C))))";
			}else
			if(name=='Simson'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Simson,Prove,configuration({A;B;C;D}:={point();point();point();point()}),incident(D,circumcircle(triangle(A,B,C)))<=>collinear(foot(D,sides(triangle(A,B,C)))))";
			}else
		    if(name=='Example197'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Example197,Prove,configuration(A:=point(),B:=point(),C:=point()),is(center(ninepointcircle(triangle(A,B,C))),midpoint(segment(Eulerpoint(A,triangle(A,B,C)),midpoint(side(B,C))))))";
			}else
		if(name=='Example198'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Example198,Prove,configuration(A:=point(),B:=point(),C:=point()),equal(times(2,length(radius(ninepointcircle(triangle(A,B,C))))),length(radius(circumcircle(triangle(A,B,C))))))";
			}else
			if(name=='Pappus'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Pappus,Prove,configuration(declare(C::Point,F::Point,P::Point,Q::Point,R::Point),A:=point(),B:=point(),D:=point(),E:=point(),give(Pappus(A,B,C,D,E,F,P,Q,R))),collinear(P,Q,R))";
			}else
			if(name=='CompleteQuandrilateral'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(CompleteQuandrilateral,Prove,configuration(A:=point(),B:=point(),C:=point(),D:=point()),collinear(midpoint(diagonal(completequadrilateral(A,B,C,D,E::Point,F::Point)))))";
			}else
			if(name=='Eulerline'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Eulerline,Prove,configuration(A:=point(),B:=point(),C:=point()),collinear(orthocenter(triangle(A,B,C)),centroid(triangle(A,B,C)),circumcenter(triangle(A,B,C))))";
			}else
			if(name=='Butterfly'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Butterfly,Prove,configuration({A;B;C}:={point();point();point()},O:=center(circle(A,B,C)),D:=pointon(circle(O,A)),E:=intersection(line(A,C),line(B,D)),l:=perpendicularline(E,line(O,E)),{F;G}:={intersection(l,line(A,D));intersection(l,line(B,C))}),is(E,midpoint(segment(F,G))))";
			}else
			if(name=='Example90'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Example90,Prove,configuration(O:=point(),O_1:=point(),A:=point(),o:=circle(O,A),o_1:=circle(O_1,A),{A;B::Point}:=intersection(o,o_1),{C::Point;E::Point}:={pointon(o);pointon(o)},{A;D::Point}:=intersection(line(A,C::Point),o_1),{B::Point;F::Point}:=intersection(line(B::Point,E::Point),o_1)),parallel(line(C::Point,E::Point),line(D::Point,F::Point)))";
			}else
			if(name=='Example180'){
				//document.getElementById('name').value = name;
				document.getElementById('statement').value="Problem(Example180,Prove,configuration(A:=point(),B:=point(),C:=point(),l:=perpendicularline(A,line(B,C)),m:=perpendicularline(C,line(A,B)),H:=intersection(l,m),o:=circle(A,B,C),{A;D}:=intersection(l,o),{C;E}:=intersection(m,o)),equal(distance(B,D),distance(B,E)))";
			}
		}
		
function fresh(){
//document.getElementById('scriptDiv').value="";
window.location.reload();
}
</script>
</head>

<body>
<form name="form1" method="post" action="draw.jsp"> 
<!--p>Problem Name: <input type="text" name="name" id="name"/></p-->
<p>Input a problem statement in GDL: </p>
<textarea method="post" type="text" name="statement" id="statement" cols="100" rows="5"></textarea>
<p>
<button type="button" onclick="Open()">Open</button> the script for 
	<select name="script" id="script"> 
        <option value="drawing">drawing</option> 
		<option value="proving">proving</option> 
     </select> 
	 <button type="button" onclick="fresh()">Clear</button>
</p>
<p> 
     <input type="Submit" value="Draw"> with
     <select name="DGS" id="DGS"> 
        <option value="GeoGebra">GeoGebra</option> 
     </select>  
</p>
<p>
	 <button type="button" onclick="Prove()">Prove</button> with
     <select name="GATP" id="GATP"> 
        <option value="GEOTHER">GEOTHER</option> 
     </select> 
</p> 
</form>
<div id="proofDiv"></div>
<div id="scriptDiv"></div>
<h3>Exmaples</h3>
<ul>
<li><p>Centroid theorem <button type="button" onclick="input('Centroid')">load</button></p><p>The three medians of a triangle are concurrent.</p>
</li>
<li><p>Simson theorem <button type="button" onclick="input('Simson')">load</button></p><p>The feet of the perpendiculars from a point to the sides of a triangle are collinear if and only if the point lies on the circumcircle of the triangle.</p>
</li>
<li><p>Example197 <button type="button" onclick="input('Example197')">load</button></p>
<p>The center of the ninepoint circle of a triangle is the midpoint of a Euler point and the midpoint of the opposite side.</p>
</li>
<li><p>Example198 <button type="button" onclick="input('Example198')">load</button></p>
<p>The radius of the nine-point circle is equal to half the circumradius of the triangle.</p>
</li>
<li><p>Pappus theorem <button type="button" onclick="input('Pappus')">load</button></p>
<p>If A, C, E are three points on one line, B, D, F on another, and if the three lines AB, CD, EF meet DE, FA, BC, respectively, then the three points of intersection L, M, N are collinear.</p>
</li>
</li>
<li><p>Complete quandrilateral theorem <button type="button" onclick="input('CompleteQuandrilateral')">load</button></p>
<p>The midpoints of the three diagonals of a complete quandrilateral are collinear.</p>
</li>
<li><p>Eulerline theorem <button type="button" onclick="input('Eulerline')">load</button></p>
<p>The orthocenter, centroid, and circumcenter of a triangle are collinear.</p>
</li>
<li><p>Butterfly theorem <button type="button" onclick="input('Butterfly')">load</button></p>
<p>A, B, C, D are four points on a circle with center O. E is the intersection of AC and BD. Through E draw a line perpendicular to OE, meeting AD and BC at F and G respectively. Then E is the midpoint of FG.</p>
</li>
<li><p>Example90 <button type="button" onclick="input('Example90')">load</button></p>
<p>Through the two common points A, B of two circles O and O_1, two lines are drawn meeting the circles at C and D, E and F, respectively. Show that CE and DF are parallel.</p>
</li>
<li><p>Example180 <button type="button" onclick="input('Example180')">load</button></p>
<p>A vertex of a triangle is the midpoint of the arc determined on its circumcircle by the two altitudes, produced, issued from the other two vertices.</p>
</li>
</ul>



</body>
</html>
